FDL - Nuprl Lemma : can-apply-p-lift

Nuprl Lemma : can-apply-p-lift

A, B:Type, P:(A

), d:(x:A

Dec(P(x))), f:({x:A| P(x)}

B), x:A.
(

can-apply(p-lift(d;f);x))

P(x)

Definitions p-lift(d;f), can-apply(f;x), b, {x:A| B(x)} , Dec(P), x:A. B(x), x(s), f(a), x:AB(x), , t T, Type, s = t, P Q, left + right, True, P Q, P & Q, P Q, A, P Q, False

Lemmas false wf, true wf, decidable wf